1. Technical Field
The present invention relates to computer program verification and decision making, and more particularly to decision making methods for programs including Boolean combinations of linear and non-linear constraints including algebraic and transcendental functions.
2. Description of the Related Art
Verification of hybrid discrete-continuous and embedded control systems may require the solving decision problems comprising Boolean combinations of linear and non-linear operations, involving transcendental and algebraic functions over reals. In general, the problem is undecidable. However, for given precision requirements, the problem becomes decidable. Therefore, one can hope that a solver can at least provide a soundness guarantee, wherein soundness implies that the solver cannot err on an unsatisfiability decision. It can also provide a completeness guarantee up to a given non-zero precision bound, wherein completeness implies that the solver cannot err on a satisfiability decision. Such guarantees are useful for analyzing instability of systems implemented using imprecise arithmetic.
There are many advanced tools in the field of Operation Research (OR) for solving linear and non-linear arithmetic optimization and feasibility problems. However, even for the linear arithmetic, these tools can give incorrect results due to the internal use of floating-point arithmetic (which is inherently imprecise due to unavoidable rounding errors). Though for OR applications such inaccuracies are acceptable in general, however for verification applications, exactness in the results is inherently important, especially, in dealing with strict inequalities and dis-equalities.
With the growing use of high-level design abstraction to capture today's complex design features, the focus of verification techniques has been shifting from propositional reasoning to decision procedures known as Satisfiability Modulo Theory (SMT) solvers. These solvers are geared towards addressing the issue of performance, without compromising the accuracy. A SMT problem for a theory T, denoted as SMT (T) comprises a Boolean combination of theory T; given a formula φ, determine whether φ is T-satisfiable, i.e., whether there exists a model of T that is also a model of φ.
Linear arithmetic OR solvers are based on precise arithmetic; however there is a significant performance hit in comparison with the SMT solvers for linear arithmetic. For any arbitrary non-zero precision, previous SMT-style approaches, based on floating-point arithmetic, are neither sound nor complete.
iSAT is a tight integration of a SAT-based proof search with interval-based arithmetic constraint propagation for reasoning over the arithmetic domain of Boolean combinations of non-linear constraints involving transcendental functions. Absolver is an SMT solver addressing a blend of Boolean and polynomial arithmetic constraint problems. It is an extensible and modular implementation of the SMT scheme which permits integration of various subordinate solvers for the Boolean, linear, and non-linear parts of the input formula. Absolver itself coordinates the overall solving process and delegates the currently active constraint sets to the corresponding subordinate solvers. For solving non-linear constraints, it uses a numerical optimization tool (IPOPT) for solving the non-linear constraints. Consequently, it may produce incorrect results due to the local nature of the solver, and due to rounding errors.